Termination Proof Script

• Consider the SCC {3,4,8,9}. By taking the AF π with π(APP) = 1 and π(app) = [1] together with the lexicographic path order with precedence f ≻ app and f ≻ s, the rules in {1,3,8} are weakly decreasing and the rules in {2,4,9} are strictly decreasing. There is one new SCC.
  • Consider the SCC {3,8}. By taking the AF π with π(APP) = 2 and π(app) = [2] together with the lexicographic path order with empty precedence, the rules in {1-3} are weakly decreasing and rule 8 is strictly decreasing. There is one new SCC.
    • Consider the SCC {3}. The constraints could not be solved.